\begin{tabbing}
1. $T$ : Type
\\[0ex]2. $T$ List
\\[0ex]3. $u$ : $T$
\\[0ex]4. $v$ : $T$ List
\\[0ex]5. \=$\forall$$x$, $y$:$T$.\+
\\[0ex]no\_repeats($T$;$v$)
\\[0ex]$\Rightarrow$ adjacent($T$;$v$;$x$;$y$)
\\[0ex]$\Rightarrow$ ($\forall$$z$:$T$. $z$ before $y$ $\in$ $v$ $\Rightarrow$ ($z$ before $x$ $\in$ $v$ $\vee$ ($z$ = $x$)))
\-\\[0ex]6. $x$ : $T$
\\[0ex]7. $y$ : $T$
\\[0ex]8. no\_repeats($T$;[$u$ / $v$])
\\[0ex]9. adjacent($T$;[$u$ / $v$];$x$;$y$)
\\[0ex]10. $z$ : $T$
\\[0ex]11. $z$ before $y$ $\in$ [$u$ / $v$]
\\[0ex]$\vdash$  $z$ before $x$ $\in$ [$u$ / $v$] $\vee$ ($z$ = $x$)
\end{tabbing}